T:Type, P:(T), L1, L2:T List.
no_repeats(T;L1)
 no_repeats(T;L2)
 (filter(P;L1) = L2
 (
 ((x:T. (x  L2)  (x  L1) & P(x)) & (x, y:T. x before y  L2  x before y  L1)) 

latex

Definitions

t  T, type List, x:AB(x), no_repeats(T;l), s = t, (x  l), b, x:AB(x), P & Q, P  Q, x:A. B(x), x before y  l, P  Q, , Type, tl(l), n-m, if a<b c ; d fi, i<j, b, ij, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, nth_tl(n;as), hd(l), l[i], n+m, Case of a; nil  s ; x.y, rec:z  t(x;y;z), x.A(x), Y, ||as||, a<b, A, AB, {x:A| B(x) }, , , Unit, left+right, f(a), nil, Prop, P  Q, P  Q, Dec(P), False, {T}, car.cdr, Void, #$n, increasing(f;k), i  j < k, {i..j}, L1  L2, filter(P;l), reduce(f;k;as), ij, A & B, x. t(x), True, SQType(T), s ~ t, T

Lemmas

squash wf, true wf, bool sq, not assert elim, l before member2, l before member, all functionality wrt iff, implies functionality wrt iff, cons before, and functionality wrt iff, iff functionality wrt iff, or functionality wrt iff, tl wf, ge wf, hd wf, non neg length, length wf1, no repeats cons, false wf, filter wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, cons member, nil member, decidable assert, iff wf, assert wf, l before wf, no repeats wf, l member wf, bool wf